1. $T$ : Type
\\[0ex]2. $m$ : $\mathbb{N}$
\\[0ex]3. $b$ : $T$
\\[0ex]4. $c$ : \{0..(0+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$
\\[0ex]$\vdash$  primrec(0+$m$;$b$;$c$) = primrec(0;primrec($m$;$b$;$c$);$\lambda$$i$,$t$. $c$($i$+$m$,$t$))